|
|
A Bit-Vector Compiler for Data-Flow Graphs
Sušovský, Tomáš ; Lengál, Ondřej (referee) ; Smrčka, Aleš (advisor)
The principal goal of this bachelor thesis is to design and implement a tool for compiling data-flow graph models to SMT-LIB format. This thesis builds on the research project HADES developed by VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The solution uses compiler for generating object model from original graph. Object model can be converted to a SMT-LIB format description including assertions of the desired system properties. Loop unrolling method (with user defined boundary for unrollment) is used for verification of system properties depending on changes in state of model. Capabilities of the developed tool are demonstrated on set of data-flow graphs models. Models cover usage of all elements defined in VAM language (input format) and their combinations. Result of this thesis presents new ways of processing data-flow graphs in VAM format and their verification.
|
|
|
PCBs Repairs with BGA and FC Packages
Buřival, Tomáš ; Špinka, Jiří (referee) ; Starý, Jiří (advisor)
Graduation thesis is specialized on dilemma of the integrated circuits with ball grid array. Chapter two describes several types of packages and confrontation of their characteristics. Chapter three considers possibilities of corrections these boards bedded with packages, mounting and demounting of these packages, method of camera control and also inspection of the soldering process. Chapter four attend to practical measuring of thermal profiles and their optimalization.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Bar Code Implemamtation to Production Process of Small Factory
Tihon, Karel ; Špinka, Jiří (referee) ; Starý, Jiří (advisor)
Target of my diploma thesis is barcode study and implementation to SMT assembly processes. This thesis contains two main parts. The first one is devoted to basic types of barcodes, reading technologies and industrial process mapping in PCB assembly. The second part is devoted to theoretical proposal and physical realization of system for materials flow monitoring. Barcode is contained in this system. Practical part of this thesis is tested in a company realizing contract manufacturing in PCB assembly - SMT and THT.
|
|
|
Mini reflow oven
Pavelka, Radek ; Jelínek, Aleš (referee) ; Burian, František (advisor)
This thesis is aimed to design a small oven for PCB soldering using the reflow method. It contains description of the oven’s construction, it’s thermodynamic parameters and the design of the control and power unit PCB as well as their control software. A remote PC control and monitoring application is also a part of this thesis.
|
|
|
Inspection of PCB with SMT by using comparative method
Hejdiš, Roman ; Stejskal, Petr (referee) ; Starý, Jiří (advisor)
The first part of the bachelor´s thesis discuss AOI, types of AOI, its utilization and importance in the industrial production. The second part is devoted to realization of simple comparative inspection method. There were testing effects of ambient light to record photographs of PCB and also artificial light was used. There was problems indication of PCB lit and PCB fixturing. At last, there are discussed some technical problems of this simple comparative method.
|
|
| |
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
|
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
|
|
|
STP solver for OpenSMT
Luňák, Václav ; Kofroň, Jan (advisor) ; Kučera, Petr (referee)
The Simple Temporal Problem is one of the fundamental scheduling problems. In the context of formal verification, it is closely related to SMT, where we can encounter it while solving the theory of difference logic. In this work we create a solver for difference logic as a part of the OpenSMT solver. We look at existing approaches and evaluate their applicability to OpenSMT. Then we analyze an algorithm based on exhaustive theory propagation and use it to create an efficient implementation of the solver. This implementation is tested and compared to other current SMT solvers, proving its comparable efficiency. 1
|
guest ::
